a,b:fpf((:Knd  Id); kz.top), z:Id.
(z  update-spec-vars(update-spec-join(a; b)))
 ((z  update-spec-vars(a))  (z  update-spec-vars(b))) 

latex

Definitions	t  T, x.A(x), x:A. B(x), x. t(x), t.2, s = t, prop{i:l}, (x  l), P  Q, x:A. B(x), f(a), map(f; as), left + right, P  Q, x:AB(x), P  Q, P  Q, P  Q, top, update-spec-vars(upd), update-spec-join(a; b), fpf(A; a.B(a)), id-deq, Kind-deq, Id, Knd, product-deq(A; B; a; b), fpf-join(eq; f; g), x:A  B(x), Type, A c B, fpf-domain(f), guard(T)
Lemmas	fpf-domain-join, fpf wf, fpf-domain wf, fpf-join wf, top wf, product-deq wf, Kind-deq wf, id-deq wf, iff functionality wrt iff, or functionality wrt iff, member map, map wf, l member wf, pi2 wf, Knd wf, Id wf